/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.symm;

import java.util.Arrays;
import java.util.Collections;
import java.util.Comparator;
import java.util.Iterator;
import java.util.List;
import java.util.Map;
import java.util.Set;

import alloy.ast.LeafId;
import alloy.bool.BooleanFormula;
import alloy.transl.ASTInfo;
import alloy.transl.ExprTransl;
import alloy.transl.RelationAllocator;
import alloy.type.BasicType;
import alloy.util.Mapper;
import alloy.util.Util;

/**
 * Symmetry-breaking for disjoint singleton sets: if the user writes
 * "some disj x,y,z: A | ..." then we can assign x={<A_0>}, y={<A_1>}, z={<A_2>}
 * without loss of generality.
 */
class SBM_DisjSingletons extends SymmetryBreakingMethod {

    SBM_DisjSingletons(ASTInfo astInfo_, RelationAllocator relAlloc_) {
        super(astInfo_, relAlloc_);
    }
    
    /**
     * Return a {@link SymmetryBreakingPredicate} for the given {@link BasicType},
     * and update the available symmetry information accordingly.  Implementations of
     * this method can assume that {@link #canBreakSymmetry} has already returned <code>true</code>
     * for this {@link AvailableSymmetry} and {@link BasicType}.
     */
    SymmetryBreakingPredicate breakSymmetry(AvailableSymmetry availSymm_,
					    Set /* of BasicType */ basicTypes_) {

	SymmetryBreakingPredicate sbp = new SymmetryBreakingPredicate();

	SubsetDetector_V subsetDetector = new SubsetDetector_V(_astInfo);
	_astInfo.getFormula().applyVisitor(subsetDetector);
	
	Map /* BasicType->List[LeafId] */ btype2disjGrp = _findDisjGrps(basicTypes_, availSymm_);
	for (Iterator btypeIter = btype2disjGrp.keySet().iterator(); btypeIter.hasNext();) {
	    BasicType btype = (BasicType)btypeIter.next();
	    List /* of LeafId */ disjGrp = (List)btype2disjGrp.get(btype);

	    System.out.println("on basic type " + btype + " disjGrp=" +
			       Util.map(disjGrp, new Mapper() { public Object map(Object obj_) {
				   return _astInfo.getLeafRep((LeafId)obj_).nodeString();
			       }}));
	    
	    int numAtomsToFix = Math.min(disjGrp.size(), btype.getScope());
	    for (int i=0; i<disjGrp.size(); i++) {
		LeafId singleton = (LeafId)disjGrp.get(i);
		ExprTransl singletonTransl = _relAlloc.getRelationTransl(singleton);
		for (int atom=0; atom<btype.getScope(); atom++) {
		    BooleanFormula atomFormula = singletonTransl.getTupleFormula(atom);
		    System.out.println("setting atom " + atom + " of " + _astInfo.getLeafRep(singleton) + " to " +
				       (atom==i));
		    sbp.conjoin(atom==i ? atomFormula : atomFormula.not());
		    if (atom==i) {
			Set /* of LeafId */ supersets = subsetDetector.getSupersets(singleton);
			for (Iterator supersetIter = supersets.iterator(); supersetIter.hasNext();) {
			    LeafId supersetId = (LeafId)supersetIter.next();
			    ExprTransl supersetTransl = _relAlloc.getRelationTransl(supersetId);
			    sbp.conjoin(supersetTransl.getTupleFormula(atom));
			}
		    }
		}
	    }
	    availSymm_.removeAllSymmetry(btype);
	    if (btype.getScope() - disjGrp.size() > 1)
		availSymm_.addSymmSet(btype, new AtomSet(disjGrp.size(), btype.getScope()));
	}
	return sbp;
    }

    /**
     * For each basic type, find the largest group of mutually disjoint singleton sets
     * on that basic type.
     * @return Map from {@link BasicType} to List of {@link LeafId}s of mutually disjoint singleton sets
     *         on that basic type.  For basic types for which the list is empty we may not have a mapping.
     */
    private Map /* BasicType->List[LeafId] */ _findDisjGrps(Set /* of BasicType */ basicTypes_, AvailableSymmetry availSymm_) {
	/*
	 * Identify unary relations that are constrained to be lone (contain at most one tuple),
	 * and those constrained to be non-empty.  (Singletons are both lone and non-empty.)
	 */
	LoneSetDetector_V loneSetDetector = new LoneSetDetector_V();
	_astInfo.getFormula().applyVisitor(loneSetDetector);
	NonemptySetDetector_V nonemptySetDetector = new NonemptySetDetector_V();
	_astInfo.getFormula().applyVisitor(nonemptySetDetector);

	/*
	 * For each fully symmetric BasicType, gather the set of singletons (non-empty lone relations) over that
	 * basic type.
	 */
	Map /* BasicType->Set[LeafId] */ btype2singletons = Util.makeMap();
	for (Iterator loneSetIter = loneSetDetector.getLoneSetIds().iterator(); loneSetIter.hasNext();) {
	    LeafId loneSetId = (LeafId)loneSetIter.next();
	    if (nonemptySetDetector.isNonemptySet(loneSetId)) {
		BasicType btype = _astInfo.getLeafType(loneSetId).getBasicTypeAt(0);
		if (availSymm_.isFullySymmetric(btype) && basicTypes_.contains(btype)) {
		    Set /* of LeafId */ thisBtypeSingletons = (Set)btype2singletons.get(btype);
		    if (thisBtypeSingletons == null)
			btype2singletons.put(btype, thisBtypeSingletons = Util.makeSet());
		    thisBtypeSingletons.add(loneSetId);
		    System.out.println("found lone set: " + _astInfo.getLeafRep(loneSetId));
		}
	    }
	}
	/**** --> remove the availSymm that we use!! ****/
	
	/*
	 * For each fully symmetric BasicType, in its list of singletons, find the largest group of singletons
	 * that are mutually disjoint.
	 */
	
	DisjDetector_V disjDetector = new DisjDetector_V();
	_astInfo.getFormula().applyVisitor(disjDetector);
	Map /* BasicType->List[LeafId] */ btype2disjGrp = Util.makeMap();
	
	for (Iterator btypeIter = btype2singletons.keySet().iterator(); btypeIter.hasNext();) {
	    BasicType btype = (BasicType)btypeIter.next();
	    Set /* of LeafId */ singletons = (Set)btype2singletons.get(btype);
	    List /* of LeafId */ largestDisjGrp = Collections.EMPTY_LIST;

	    for (Iterator singletonIter = singletons.iterator(); singletonIter.hasNext();) {
		LeafId thisSingleton = (LeafId)singletonIter.next();
		Set /* of LeafId */ disjFromThis = disjDetector.getRelsDisjFrom(thisSingleton);
		if (disjFromThis.size() > largestDisjGrp.size()) {
		    /* check whether the singletons in disjFromThis are pairwise disjoint */
		    LeafId[] disjGrp = (LeafId[])disjFromThis.toArray(new LeafId[]{});
		    boolean pairwiseDisjoint = true;
		    for (int i=0; pairwiseDisjoint && i<disjGrp.length; i++)
			for (int j=i+1; pairwiseDisjoint && j<disjGrp.length; j++)
			    if (!disjDetector.relationsAreDisjoint(disjGrp[i], disjGrp[j]))
				pairwiseDisjoint = false;
		    if (pairwiseDisjoint)
			largestDisjGrp = Arrays.asList(disjGrp);
		}
	    }

	    if (largestDisjGrp.size() < 1)
		largestDisjGrp = Collections.singletonList(singletons.iterator().next());

	    if (largestDisjGrp.size() > 1)
		Collections.sort(largestDisjGrp, new Comparator() { public int compare(Object obj1_, Object obj2_) {
		    int cmp = obj1_.toString().compareTo(obj2_.toString());
		    if (cmp != 0)
			return cmp;
		    LeafId id1 = (LeafId)obj1_;
		    LeafId id2 = (LeafId)obj2_;
		    return id1.compareTo(id2);
		}});

	    btype2disjGrp.put(btype, largestDisjGrp);
	}

	return btype2disjGrp;
    }  // _findDisjointSingletons()
}
